x:(), r:, a:, k:, y:( List).
(k  ||y||)
 ((r = 0)  0 < a  (0  a & r = 1))
 q-rel(r;q-linear(k;j.x(j);y))
 q-rel(r;q-linear(k;j.a * (x(j));y)) 

latex

Definitions

(i = j), qeq(r;s), i <z j, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.2, t.1, , x f y, b, a  b, r * s, r  s, ff, tt, if b then t else f fi , {T}, SQType(T), x. t(x), t  T, True, T, , P  Q, P  Q, q-rel(r;x), P & Q, P  Q, P  Q, x:A. B(x), Dec(P), Unit, , False, A, x(s), A  B, , , S  T

Lemmas

qle antisymmetry, qless complement qorder, decidable qless, qmul zero qrng, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, qmul preserves qless, qmul preserves qle, not wf, bnot wf, qmul comm qrng, qmul wf, assert wf, bool wf, eq int wf, length wf1, le wf, qle wf, int inc rationals, qless wf, nat wf, q-linear wf, q-linear-times, rationals wf, true wf, squash wf, q-rel wf